[Giesl and Middeldorp - JFP'04, Example 49]

Example 49 in [Giesl and Middeldorp - JFP'04]

Summary: Ex49_GM04

CS-TRS Ex49_GM04 (file Ex49_GM04.csr)

Functions:  minus 0 s geq true false div if

Constructors:  0 s true false

Variables:  Y X

Arities: 

ar(minus) = 2
ar(0) = 0
ar(s) = 1
ar(geq) = 2
ar(true) = 0
ar(false) = 0
ar(div) = 2
ar(if) = 3

Replacement map: 

µ(minus)={}
µ(0)={}
µ(s)={1}
µ(geq)={}
µ(true)={}
µ(false)={}
µ(div)={1}
µ(if)={1}

Rules: (file Ex49_GM04)   

minus(0,Y) -> 0
minus(s(X),s(Y)) -> minus(X,Y)
geq(X,0) -> true
geq(0,s(Y)) -> false
geq(s(X),s(Y)) -> geq(X,Y)
div(0,s(Y)) -> 0
div(s(X),s(Y)) -> if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)
if(true,X,Y) -> X
if(false,X,Y) -> Y

The CS-TRS in OBJ format (file Ex49_GM04.obj):

obj Ex49_GM04 is
  sort S .
  op minus : S S -> S [strat (0)] .
  op 0 : -> S .
  op s : S -> S .
  op geq : S S -> S [strat (0)] .
  op true : -> S .
  op false : -> S .
  op div : S S -> S [strat (1 0)] .
  op if : S S S -> S [strat (1 0)] .
  vars Y X : S .
  eq minus(0,Y) = 0 .
  eq minus(s(X),s(Y)) = minus(X,Y) .
  eq geq(X,0) = true .
  eq geq(0,s(Y)) = false .
  eq geq(s(X),s(Y)) = geq(X,Y) .
  eq div(0,s(Y)) = 0 .
  eq div(s(X),s(Y)) = if(geq(X,Y),s(div(minus(X,Y),s(Y))),0) .
  eq if(true,X,Y) = X .
  eq if(false,X,Y) = Y .
endo

Negative results

  1. The µ-termination of Ex49_GM04 cannot be proved by using Lucas' transformation: The TRS Ex49_GM04_L: 
        minus -> 0
    minus -> minus
    geq -> true
    geq -> false
    geq -> geq
    div(0) -> 0
    div(s(X)) -> if(geq)
    if(true) -> X
    if(false) -> Y
    contains extra variables.

Positive results

  1. The TRS Ex49_GM04 (without replacement restrictions): 
        minus(0,Y) -> 0
    minus(s(X),s(Y)) -> minus(X,Y)
    geq(X,0) -> true
    geq(0,s(Y)) -> false
    geq(s(X),s(Y)) -> geq(X,Y)
    div(0,s(Y)) -> 0
    div(s(X),s(Y)) -> if(geq(X,Y),s(div(minus(X,Y),s(Y))),0)
    if(true,X,Y) -> X
    if(false,X,Y) -> Y
    is terminating (use MuTerm).
  2. The µ-termination of Ex49_GM04 can be proved by using Zantema's transformation. The TRS Ex49_GM04_Z: 
        minus(n__0,Y) -> 0
    minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
    geq(X,n__0) -> true
    geq(n__0,n__s(Y)) -> false
    geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
    div(0,n__s(Y)) -> 0
    div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0)
    if(true,X,Y) -> activate(X)
    if(false,X,Y) -> activate(Y)
    0 -> n__0
    s(X) -> n__s(X)
    activate(n__0) -> 0
    activate(n__s(X)) -> s(X)
    activate(X) -> X
    is terminating (use MuTerm).
  3. By [GM04, Theorem 11], the µ-termination of Ex49_GM04 can also be proved by using Ferreira and Ribeiro's transformation (but no concrete proof has been reported yet).
  4. The µ-termination of Ex49_GM04 is proved in [GM04, Example 49 & Appendix D] by using Giesl and Middeldorp's transformation. The TRS Ex49_GM04_GM: 
        a__minus(0,Y) -> 0
    a__minus(s(X),s(Y)) -> a__minus(X,Y)
    a__geq(X,0) -> true
    a__geq(0,s(Y)) -> false
    a__geq(s(X),s(Y)) -> a__geq(X,Y)
    a__div(0,s(Y)) -> 0
    a__div(s(X),s(Y)) -> a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0)
    a__if(true,X,Y) -> mark(X)
    a__if(false,X,Y) -> mark(Y)
    mark(minus(X1,X2)) -> a__minus(X1,X2)
    mark(geq(X1,X2)) -> a__geq(X1,X2)
    mark(div(X1,X2)) -> a__div(mark(X1),X2)
    mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
    mark(0) -> 0
    mark(s(X)) -> s(mark(X))
    mark(true) -> true
    mark(false) -> false
    a__minus(X1,X2) -> minus(X1,X2)
    a__geq(X1,X2) -> geq(X1,X2)
    a__div(X1,X2) -> div(X1,X2)
    a__if(X1,X2,X3) -> if(X1,X2,X3)
    is terminating (use AProVE).
  5. The µ-termination of Ex49_GM04 is also proved in [Luc04, Example 7] by using a polynomial interpretation: 
        [minus](x,y) = x + 1
    [s](x) = x + 3
    [geq](x,y) = x + 2
    [div](x,y) = x^2 + x + 1
    [if](x,y,z) = xz + x + y + 1
    [0] = 0
    [true] = 0
    [false] = 1
  6. The µ-termination of Ex49_GM04 can be proved by using the refinement of CSRPO described in [Bor03, Section 3.3.12].